Problem: f(f(a())) -> f(g(n__f(a()))) f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {5,4} transitions: f1(24) -> 25* f1(26) -> 27* f1(18) -> 19* n__f1(10) -> 11* n__f1(16) -> 17* n__f1(8) -> 9* n__f2(30) -> 31* n__f2(36) -> 37* n__f2(38) -> 39* f0(2) -> 4* f0(1) -> 4* f0(3) -> 4* a0() -> 1* g0(2) -> 2* g0(1) -> 2* g0(3) -> 2* n__f0(2) -> 3* n__f0(1) -> 3* n__f0(3) -> 3* activate0(2) -> 5* activate0(1) -> 5* activate0(3) -> 5* 1 -> 5,24,10 2 -> 5,18,16 3 -> 5,26,8 9 -> 4* 11 -> 4* 17 -> 4* 18 -> 36* 19 -> 5* 24 -> 38* 25 -> 5* 26 -> 30* 27 -> 5* 31 -> 27* 37 -> 19,5 39 -> 25,5 problem: Qed